\begin{tabbing}
$\forall$$x_{1}$:es\_realizer\{i:l\}. 
\\[0ex]($\uparrow$Rsends?($x_{1}$))
\\[0ex]$\Rightarrow$ (\=Rsends{-}g($x_{1}$)\+
\\[0ex]$\in$ (\=(${\it tg}$:Id\+
\\[0ex]$\times$ (decl{-}state(Rsends{-}ds($x_{1}$))$\rightarrow$Rsends{-}T($x_{1}$)$\rightarrow$(decl{-}type\=\{i:l\}\+
\\[0ex](\=Rsends{-}dt($x_{1}$); ${\it tg}$\+
\\[0ex]) List))) List))
\-\-\-\-
\end{tabbing}